Inference at * 2 
Iof proof for Lemma branch wf2:

.....subterm..... T:t3:n

1. P : 
2. d : Dec(P)
3. T : Type
4. PT
5. B : q:P.T
6. x : P
7. d = (inr x )
  B  T 

latex

 by ((With x (D 5)) 
CollapseTHEN (Auto)) 

latex

Co.

Definitions

x:A.B(x), t  T